YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { admit(x, nil()) -> nil()
  , admit(x, .(u, .(v, .(w(), z)))) ->
    cond(=(sum(x, u, v), w()),
         .(u, .(v, .(w(), admit(carry(x, u, v), z)))))
  , cond(true(), y) -> y }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping

 safe(admit) = {1}, safe(nil) = {}, safe(.) = {1, 2}, safe(w) = {},
 safe(cond) = {1, 2}, safe(=) = {1, 2}, safe(sum) = {1, 2, 3},
 safe(carry) = {1, 2, 3}, safe(true) = {}

and precedence

 admit > cond .

Following symbols are considered recursive:

 {admit}

The recursion depth is 1.

For your convenience, here are the satisfied ordering constraints:

                           admit(nil(); x) > nil()                                                            
                                                                                                              
  admit(.(; u,  .(; v,  .(; w(),  z))); x) > cond(; =(; sum(; x,  u,  v),  w()),                              
                                                    .(; u,  .(; v,  .(; w(),  admit(z; carry(; x,  u,  v))))))
                                                                                                              
                        cond(; true(),  y) > y                                                                
                                                                                                              

Hurray, we answered YES(?,O(n^1))